Conversation
…e-test patterns + Zeta plugin-adapter as worked example (Aaron 2026-05-05) Aaron 2026-05-05 forwarded the Claude.ai shard's RFC pre-draft + verbatim "you can make it a candidate" -- using Zeta's plugin adapter (src/Core/PluginApi.fs:103-132) as the worked-example anchor for the RFC's motivation section. The proposal: allow F#'s type-test syntax (:?) to use wildcard placeholders for generic type parameters, enabling tests like :? IBilinearOperator<_, _, 'TOut> for runtime detection of plugins implementing capability interfaces with unknown input type parameters. Pre-draft NOT submitted -- verification preconditions documented (prior fslang-suggestions threads, fslang-design in-flight RFCs, Don Syme's prior work, benchmark vs direct :?, C# csharplang coordination). Per Aaron 2026-05-05: Don Syme (creator of F#, MSR Cambridge) is the F# human anchor. Not authority-by-position, but the load- bearing intellectual reference for any type-system extension. Any RFC of this scope must engage his prior treatment of existential quantification before submission, not silently omit. Mirror-not-beacon discipline per PR #1575 / #1582 / #1588. The RFC is a candidate, not authority. Submission upstream is downstream work; this file preserves the pre-draft for future-Otto reference. What this file does NOT do: - Submit the RFC (verification preconditions + Aaron's go-ahead) - Establish authorship (Claude.ai shard text + Zeta worked-example anchor; final submission carries F# lang-design attribution) - Promise acceptance (RFCs go through community review) - Bundle the "Zeta extended DBSP and found a bug in the 2023 paper" claim into a metaphysical assertion -- empirical context for why the worked example is real, not a glass-halo flex Composes with B-0194 (PR #1589 -- the in-flight backlog row using the same plugin-adapter substrate), src/Core/Units.fs (PR #1590 -- Pragmatics section UoM-as-precedent reference), PR #1588 (parent Claude.ai conversation). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
deleted the
research/fsharp-rfc-existential-quantification-pre-draft-aaron-2026-05-05
branch
There was a problem hiding this comment.
Pull request overview
Adds a research-grade preservation of a candidate F# language RFC (pre-draft) proposing wildcard/existential generic parameters in :? type-test patterns, using Zeta’s plugin adapter as the motivating worked example and documenting verification preconditions before any upstream submission.
Changes:
- Add a new
docs/research/**entry capturing the RFC pre-draft text, motivation, and design sketch. - Document verification preconditions (prior-art search, perf benchmark, C# cross-check, linkability).
- Provide a Zeta plugin-capability detection scenario as the anchor use case.
| let (|Bilinear|_|) (op: obj) = | ||
| op.GetType().GetInterfaces() | ||
| |> Array.tryPick (fun i -> | ||
| if i.IsGenericType && i.GetGenericTypeDefinition() = typedefof<IBilinearOperator<_,_,_>> |
|
|
||
| ### Real-world demand: Zeta's plugin adapter (the worked-example anchor) | ||
|
|
||
| The Zeta project (an F# DBSP implementation that has extended the published 2023 DBSP algebra and identified a bug in the original paper) declares four runtime-detectable algebra-capability interfaces in `src/Core/PluginApi.fs:103-132`: |
Comment on lines
+144
to
+149
| - `docs/backlog/P2/B-0194-incremental-auto-dispatcher-bilinear-capability-detection-aaron-2026-05-05.md` (PR #1589) -- the in-flight backlog row this RFC's worked-example anchor connects to. | ||
| - `src/Core/PluginApi.fs:103-132` -- the four capability interfaces that motivate the existential-quantification need. | ||
| - `src/Core/Units.fs` (PR #1590, in flight) -- the Pragmatics section's UoM-as-precedent reference points at it. | ||
| - `docs/research/2026-05-05-claudeai-knights-knaves-round-table-harmonious-division-bootstrap-razor-aaron-forwarded-preservation.md` (PR #1588) -- the parent Claude.ai conversation that produced the initial F# type-system analysis. | ||
| - F# language-design canonical surfaces: `https://github.com/fsharp/fslang-suggestions` (suggestions), `https://github.com/fsharp/fslang-design` (RFCs). | ||
| - C# language-design canonical surface: `https://github.com/dotnet/csharplang`. |
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…-05-05 same-tick)
Aaron 2026-05-05 added two pieces of context after the initial
subagent draft was committed:
1. **Four-property hodl invariant as binding acceptance test**:
DST-safe + lock-free + scale-free + DBSP-native must all hodl
for any numeric-type candidate. NOT separable -- relaxing any
one lets bugs through (the Prop 3.5 misattribution caught
earlier this session is a worked example). Composes with the
"DST hodls everywhere" lineage at memory/feedback_aaron_class_
discovery_experiment_rodney_razor_on_self_dst_holds_everywhere
_aaron_2026_05_01.md. Per-candidate acceptance scoring against
the conjunction, not score-against-overflow-prevention-alone.
2. **Human anchors** named:
- **Tanner Gooding** (.NET runtime, generic math interfaces) --
primary anchor for SRTP-replacement-for-numeric-typeclass shape
- **Don Syme** (F# language) -- stays the F# anchor for
language-extension work (RFC #1591); numerics-runtime goes
through Gooding
- **Leonid Ryzhyk (@ryzhyk)** (DBSP / Feldera GitHub) --
ENGAGEMENT GATE: only engage IF a real DBSP-compatibility
finding lands (cross-check first; speculative findings don't
reach external engagement -- the Prop 3.5 misattribution was
itself a worked example of why).
Carved-sentence-wise: "BigDecimal-with-rounding may NOT satisfy
DBSP-native (rounding errors don't necessarily compose with
negation)" is one operationally testable per-candidate result.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…-05-05 same-tick)
Aaron 2026-05-05 added two pieces of context after the initial
subagent draft was committed:
1. **Four-property hodl invariant as binding acceptance test**:
DST-safe + lock-free + scale-free + DBSP-native must all hodl
for any numeric-type candidate. NOT separable -- relaxing any
one lets bugs through (the Prop 3.5 misattribution caught
earlier this session is a worked example). Composes with the
"DST hodls everywhere" lineage at memory/feedback_aaron_class_
discovery_experiment_rodney_razor_on_self_dst_holds_everywhere
_aaron_2026_05_01.md. Per-candidate acceptance scoring against
the conjunction, not score-against-overflow-prevention-alone.
2. **Human anchors** named:
- **Tanner Gooding** (.NET runtime, generic math interfaces) --
primary anchor for SRTP-replacement-for-numeric-typeclass shape
- **Don Syme** (F# language) -- stays the F# anchor for
language-extension work (RFC #1591); numerics-runtime goes
through Gooding
- **Leonid Ryzhyk (@ryzhyk)** (DBSP / Feldera GitHub) --
ENGAGEMENT GATE: only engage IF a real DBSP-compatibility
finding lands (cross-check first; speculative findings don't
reach external engagement -- the Prop 3.5 misattribution was
itself a worked example of why).
Carved-sentence-wise: "BigDecimal-with-rounding may NOT satisfy
DBSP-native (rounding errors don't necessarily compose with
negation)" is one operationally testable per-candidate result.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…gration (Aaron 2026-05-05) (#1595) * backlog(P2): B-0196 BigInt + BigRational + BigDecimal + BigFloat integration -- substrate survey + per-class adoption recommendation (Aaron 2026-05-05) Aaron 2026-05-05 verbatim "oh backlog bigint and other bitnumbers integration" -- surfaced after a reviewer caught int64 overflow in Units.msToNs (PR #1590, fixed via Checked.(*) + 3 overflow tests). The msToNs case is one instance of a broader question this row owns: should Zeta support arbitrary-precision integers (BigInteger), arbitrary-precision rationals (BigRational), arbitrary-precision decimals (BigDecimal), and arbitrary-precision floats (BigFloat / MPFR-style) for cases where int64 / double overflow or precision- loss is in the operating regime? Research + plan row, NOT implementation. Output is a survey + per- numeric-class adoption recommendation; doing any swap that turns out to be warranted is a separate row filed downstream. Five concrete shapes covered: BigInteger (.NET System.Numerics), BigRational (exact probability arithmetic), BigDecimal (financial, LFG context), MPFR-style BigFloat (scientific), and SRTP-based generic numerics (numeric type-class abstraction). Acceptance criteria with falsifiability hooks: - (a) Substrate survey -- baseline numbers in row: ~470 raw int64|float|double mentions in src/Core, 40 Checked.* arithmetic guard sites across 12 files. - (b) Risk-site identification -- 5 starting candidates each with operating regime + falsifier: msToNs, Z-set weight aggregation, IndexedZSet bilinear delta product, BayesianAggregate (BetaBernoulli / NormalGamma / DirichletMultinomial), TimeSeries window arithmetic. - (c) Decision -- per-class adoption vs system-wide generic-numerics refactor vs defer-until-second-overflow-site (carved-sentence default). - (d) F# UoM compatibility note -- BigInteger likely not on the F# spec's allowed-measure-types list; needs WebSearch verification per Otto-364 search-first authority. Carved sentence: *"Pick numerics by where the regime fires; per- class adoption beats a system-wide refactor until the second overflow site lands. The msToNs fix is a Checked-throws guard, not yet a BigInteger argument; the second site is the trigger."* Composes with B-0140 / B-0156 (TS+Bun BigInt sister), B-0189 (Q# Bayesian -- where precision matters), B-0194 (capability dispatcher -- where the bilinear-product overflow lives). P2 (not P1, not P3): higher than P3 because real trigger (PR #1590 reviewer caught overflow) and Aaron explicitly named the row; lower than P1 because the Checked.* guard already shipped is sufficient for correctness, and the BigInteger / BigRational / BigDecimal decision is research-grade, not blocking. Substrate-or-it-didn't-happen (Otto-363): converts Aaron's chat- weather framing into a falsifiable durable research artifact. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): four-property hodl invariant + human anchors (Aaron 2026-05-05 same-tick) Aaron 2026-05-05 added two pieces of context after the initial subagent draft was committed: 1. **Four-property hodl invariant as binding acceptance test**: DST-safe + lock-free + scale-free + DBSP-native must all hodl for any numeric-type candidate. NOT separable -- relaxing any one lets bugs through (the Prop 3.5 misattribution caught earlier this session is a worked example). Composes with the "DST hodls everywhere" lineage at memory/feedback_aaron_class_ discovery_experiment_rodney_razor_on_self_dst_holds_everywhere _aaron_2026_05_01.md. Per-candidate acceptance scoring against the conjunction, not score-against-overflow-prevention-alone. 2. **Human anchors** named: - **Tanner Gooding** (.NET runtime, generic math interfaces) -- primary anchor for SRTP-replacement-for-numeric-typeclass shape - **Don Syme** (F# language) -- stays the F# anchor for language-extension work (RFC #1591); numerics-runtime goes through Gooding - **Leonid Ryzhyk (@ryzhyk)** (DBSP / Feldera GitHub) -- ENGAGEMENT GATE: only engage IF a real DBSP-compatibility finding lands (cross-check first; speculative findings don't reach external engagement -- the Prop 3.5 misattribution was itself a worked example of why). Carved-sentence-wise: "BigDecimal-with-rounding may NOT satisfy DBSP-native (rounding errors don't necessarily compose with negation)" is one operationally testable per-candidate result. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): bidirectional composes_with + NormalGamma->NormalInverseGamma + tools/z3->tools/Z3Verify + + bullet + BayesianAggregate Checked correction (#1595 reviewer) Seven reviewer threads addressed: 1. **Bidirectional composes_with** (per tools/backlog/README.md:69-70): added B-0196 to B-0140, B-0156, B-0189, B-0194's composes_with lists. B-0140 + B-0156 had no composes_with field; created. 2. **`+` continuation bullet** at line 139 broke markdownlint MD007 (parsed as nested + list). Changed `+ provides a count` to `AND provides a count`. 3+5. **NormalGamma -> NormalInverseGamma**: BayesianAggregate.fs has NormalInverseGamma, not NormalGamma. Sed-corrected at all occurrences. 4. **BayesianAggregate Checked.* survey baseline**: reviewer correctly noted BayesianAggregate.fs has no Checked.* arithmetic guards (only one doc-comment mention). The original subagent's listing was wrong. Corrected with explicit acknowledgment + note that Bayesian surfaces use double arithmetic without checked guards (different shape from int64- overflow risk; relevant to BigRational candidate, not BigInteger). 6. **Units.fs cross-reference**: was stale at PR time. Now resolves on main since #1590 merged. 7. **tools/z3/ -> tools/Z3Verify/**: corrected dead path reference. Regenerated docs/BACKLOG.md. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): markdownlint MD032 + MD018 + last_updated bumps for B-0156/B-0189 (#1595 reviewer follow-up) Three reviewer + CI findings: 1. MD032/blanks-around-lists at line 148: list "- src/Core ..." needed blank line before. Fixed. 2. MD018/no-missing-space-atx at line 412: "#1590 with Checked.(*)..." at line-start parsed as ATX heading. Rephrased "PR #1590" to "PR 1590" in the soft-wrapped paragraph; ATX-collision avoided. 3. last_updated bumps: B-0156 (2026-05-01 -> 2026-05-05) and B-0189 (2026-05-04 -> 2026-05-05) had frontmatter edits adding B-0196 to composes_with but kept stale dates. Bumped per tools/backlog/README.md schema requirement. Regenerated docs/BACKLOG.md. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): soften UoM-on-BigInteger pre-answer to hypothesis-with-search-required (#1595 reviewer) Reviewer correctly caught: section (b) asserted as fact ("F# UoM is constrained to primitive numeric types per the F# spec; this is itself a substantive finding") what section (d) treats as unverified research. Pre-answering one's own research question is the failure mode the four-property hodl is meant to catch -- the training-data prior was leaking through as if it were verified fact, contradicting Otto-364 search-first authority. Reframed: BigInteger<weight> is a hypothesis to test. The expected training-data answer is the primitive-numeric-types constraint, but that hypothesis must be WebSearch-verified against current upstream documentation before binding. Recent F# versions may have lifted the constraint, or community workarounds (measure-attributed wrapper structs) may exist. Section (d) is the research task that resolves this. The two stale last_updated reviewer threads (PRRT_kwDOSF9kNM5_kaHu on B-0140, PRRT_kwDOSF9kNM5_kaIL on B-0194) are reviewer-snapshot stale -- e582f38 already bumped B-0140 to 2026-05-05, and B-0194 was created at 2026-05-05 from origin. Both currently correct on the branch. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…orb-and-contribute (Aaron 2026-05-05) (#1596) * backlog(P3): B-0198 F# UoM-on-BigInteger upstream contribution -- absorb-and-contribute (Aaron 2026-05-05) Aaron 2026-05-05 verbatim, after PR #1596 verified F# UoM does not natively extend to System.Numerics.BigInteger: "but no implementation. do they need help we are good neighbors and citizens of github and our dependencies" Per memory/feedback_absorb_and_contribute_community_dependency_ discipline_2026_04_22.md: when Zeta depends on community work AND identifies a gap, contributing back is the discipline. Two contribution shapes: Option 1 (lightweight): comment on fslang-suggestions/831 surfacing Zeta's BigInteger<weight> use case as evidence-of-demand. Cost-free, citizen-move signal that the gap is felt downstream. Option 2 (heavier): RFC pre-draft for UoM-extension-to-BigInteger specifically (separate from generic-arithmetic/831), following PR 1591's pattern. Verification preconditions documented (search fslang-suggestions, fslang-design, Don Syme prior work, csharplang coordination). P3 because: - Not blocking Zeta (in-language workarounds suffice for B-0196's per-class adoption decision) - Citizenship work, not survival work - Bounded scope per option Engagement gate: only escalate IF contribution has substance -- the Prop 3.5 misattribution worked example shows premature upstream engagement on under-verified findings is itself the failure mode. Composes with B-0196, PR #1591, the absorb-and-contribute discipline memory file, and fslang-suggestions/831. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0198): MD027 blockquote single-space + bidirectional composes_with on B-0196 (#1596 reviewer) Two real reviewer findings: 1. MD027/no-multiple-space-blockquote at line 24:3 -- the verbatim blockquote had double-space after `>`. Reduced to single-space. The verbatim text content is preserved unchanged. 2. Bidirectional composes_with: B-0196 now lists B-0198 in its composes_with frontmatter. The edge B-0198 -> B-0196 already existed; this adds B-0196 -> B-0198 making it bidirectional per tools/backlog/README.md schema. The third "github -> GitHub in row title" reviewer thread is a false-positive: the row title contains no "github" string at all. Lowercase "github" appears only in (a) the verbatim ask: field quote (preserve as-is per witnessable-evolution), (b) the verbatim blockquote at line 23-24 (preserve as-is), (c) inside markdown URL paths like https://github.com/... (correct lowercase per URL convention). No title change needed. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Aaron 2026-05-05 forwarded Claude.ai shard's pre-draft of an F# RFC for allowing
:?type-test syntax to use_wildcards on generic type parameters (so:? IBilinearOperator<_, _, 'TOut>works for runtime detection where the input types are existentially quantified).Aaron explicit: "you can make it a candidate" using Zeta's plugin adapter (
src/Core/PluginApi.fs:103-132) as the worked-example anchor.Per Aaron 2026-05-05: Don Syme is the F# human anchor
Creator of F#, MSR Cambridge, original F#-ML architect. Any RFC of this scope must engage his prior treatment of existential quantification before submission, not silently omit. Verification precondition added.
Pre-draft NOT submitted
Verification preconditions documented:
fsharp/fslang-suggestionsfor existing threadsfsharp/fslang-designfor in-flight RFCs:?dotnet/csharplangMirror-not-beacon discipline
Per PR #1575 / #1582 / #1588 lineage. The RFC is a candidate, not authority. Submission upstream is downstream work.
Composes with
🤖 Generated with Claude Code